M:MsgA, k:Knd, s:M.state, v:M.da(k). ma-has-effect(M;k)  (x.M.ef(k,x,s,v)?s(x)) = s 

latex

Definitions	State(ds), M.state, t  T, M.ef(k,x,s,v)?w, M.ds(x), Id, x:A. B(x), 1of(t), Top, f(x)?z, MsgA, Knd, M.da(a), ma-has-effect(M;k), A, P  Q, False, b, b, , Prop, x. t(x), 2of(t), IdDeq, KindDeq, a:A fp B(a), product-deq(A;B;a;b), x  dom(f), P & Q, P  Q, Unit, Valtype(da;k), (x  l), x:A. B(x), P  Q, map(f;as)
Lemmas	assert-deq-member, map wf, member map, l member wf, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, fpf-dom wf, product-deq wf, fpf-trivial-subtype-top, ma-state wf, Kind-deq wf, pi1 wf, top wf, fpf-cap wf, id-deq wf, pi2 wf, bool wf, bnot wf, assert wf, not wf, ma-has-effect wf, ma-da wf, ma-st wf, Knd wf, msga wf, ma-ef-val wf, Id wf